$\forall$$T$:Type, $L$:$T$ List, $R$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$) \}$\rightarrow$Realizer), $A$:Realizer. \\[0ex]$A$ $\parallel$ $\oplus$$x$$\in$$L$.$R$($x$) $\Leftrightarrow$ ($\forall$$x$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ $A$ $\parallel$ $R$($x$))